/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXB30/FONT#2=BAXI30[  J,RED]/FONT#3=SUB/FONT#4=SET1/FONT#5=NGR20/FONT#6=GRK30/FONT#7=SUP/FONT#8=SPEC[  J,RED]/FONT#9=BDR40/FONT#10=MATH30/FONT#11=METSB/FONT#12=NONMBI/FONT#13=GERM35/FONT#14=MG[LSP,JRA]/FONT#16=NGB30/FONT#15=ZERO30



␈↓ α∧␈↓␈↓ ¬W␈↓↓Introduction␈↓

␈↓"∀␈↓ α∧␈↓Software␈α∪is␈α∪expensive␈α∩and,␈α∪too␈α∪often,␈α∩bug␈α∪ridden.␈α∪ Debugging␈α∩is␈α∪still␈α∪the␈α∩most
␈↓ α∧␈↓commonly␈α∂used␈α⊂method␈α∂of␈α∂increasing␈α⊂confidence␈α∂in␈α∂the␈α⊂correctness␈α∂of␈α⊂a␈α∂program.
␈↓ α∧␈↓Proving␈α∪the␈α∪correctness␈α∀of␈α∪programs␈α∪is␈α∀difficult.␈α∪ Many␈α∪approaches␈α∀have␈α∪been
␈↓ α∧␈↓proposed␈αto␈αensure␈αreliable␈αprograms,␈α
some␈αdealing␈αwith␈αthe␈α programming␈αtask␈α
and
␈↓ α∧␈↓others with proving a completed program meets its specifications.

␈↓ α∧␈↓␈↓ αdSeveral␈α∩automatic␈α⊃verification␈α∩systems␈α⊃have␈α∩been␈α⊃constructed␈α∩for␈α⊃proving
␈↓ α∧␈↓verification␈αconditions␈αin␈αa␈αspecific␈αproblem␈αdomain;␈αthey␈αemploy␈αstrategies␈αthat␈αare
␈↓ α∧␈↓geared␈αto␈αthat␈αdomain,␈αthus␈αthe␈αability␈αto␈αhandle␈αproblems␈αin␈αa␈αnew␈αsubject␈αdomain
␈↓ α∧␈↓typically␈αrequires␈αextensive␈αmodifications␈αof␈αthe␈αsystem.␈α A␈αmuch␈αharder␈αproblem␈αis
␈↓ α∧␈↓discovery␈α∃of␈α⊗the␈α∃verification␈α∃conditions␈α⊗themselves.␈α∃ One␈α∃must␈α⊗find␈α∃assertions
␈↓ α∧␈↓(statements␈α⊗of␈α⊗first-order␈α∃logic)␈α⊗that␈α⊗characterize␈α∃the␈α⊗desired␈α⊗behavior␈α⊗of␈α∃the
␈↓ α∧␈↓program.␈α
 It␈α
is␈α
possible␈α
to␈α∞generate␈α
some␈α
of␈α
these␈α
assertions␈α
automatically␈α∞from␈α
the
␈↓ α∧␈↓text␈α⊃of␈α⊃the␈α⊃program,␈α⊃but␈α∩the␈α⊃programmer␈α⊃must␈α⊃supply␈α⊃the␈α⊃critical␈α∩assertions␈α⊃on
␈↓ α∧␈↓which␈α∞the␈α
program␈α∞was␈α∞based.␈α
 The␈α∞assertions␈α
thus␈α∞derived␈α∞are␈α
referred␈α∞to␈α∞as␈α
the
␈↓ α∧␈↓␈↓αspecifications␈↓␈α∪of␈α∪the␈α∩program.␈α∪Whether␈α∪such␈α∪a␈α∩derivation␈α∪is␈α∪done␈α∪manually␈α∩or
␈↓ α∧␈↓automatically,␈α∪we␈α∪believe␈α∪the␈α∀approach␈α∪is␈α∪backward.␈α∪ The␈α∪entire␈α∀process␈α∪seems
␈↓ α∧␈↓analogous to building a house, then measuring the house  to construct the blueprints.

␈↓ α∧␈↓␈↓ αdSpecifications␈αshould␈αbe␈α
written␈αfirst,␈αthen␈αa␈α
program␈αmay␈αbe␈α
constructed␈αto
␈↓ α∧␈↓fit␈α
its␈α
specifications␈α
just␈α
as␈α
a␈αhouse␈α
is␈α
constructed␈α
according␈α
to␈α
its␈α
blueprints.␈αA␈α
proof
␈↓ α∧␈↓that␈α⊃a␈α⊃program␈α⊃meets␈α⊃certain␈α⊃specifications␈α⊃should␈α⊃be␈α⊃developed␈α⊃along␈α∩with␈α⊃the
␈↓ α∧␈↓program␈α∩itself,␈α∩or␈α∩guaranteed␈α∩through␈α∩the␈α∩use␈α∩of␈α∩rules␈α∩that␈α∩have␈α∪already␈α∩been
␈↓ α∧␈↓proven valid to transform the specification into a program.

␈↓ α∧␈↓␈↓ αdThe␈α
specification␈αshould␈α
be␈α
written␈αin␈α
a␈α
high␈αlevel␈α
language␈α
that␈αenables␈α
one
␈↓ α∧␈↓to␈α∞describe␈α
what␈α∞is␈α
to␈α∞be␈α
accomplished,␈α∞indicating␈α
functional␈α∞relationships,␈α
without
␈↓ α∧␈↓considering␈α∞computational␈α
details.␈α∞ Such␈α
a␈α∞specification,␈α
in␈α∞which␈α
only␈α∞the␈α
abstract
␈↓ α∧␈↓description␈α∃of␈α∀the␈α∃program␈α∃is␈α∀required,␈α∃is␈α∀less␈α∃prone␈α∃to␈α∀error␈α∃than␈α∃a␈α∀typical
␈↓ α∧␈↓programming␈α
language␈αspecification␈α
in␈αwhich␈α
every␈αdetail␈α
of␈αthe␈α
computation␈αmust
␈↓ α∧␈↓be␈α
provided.␈α The␈α
problems␈αof␈α
incomplete␈α
or␈αincorrect␈α
specifications␈αdo␈α
not␈αgo␈α
away,
␈↓ α∧␈↓however, they are more tractable with this approach.

␈↓ α∧␈↓␈↓ αdProgram␈α⊂synthesis␈α⊃is␈α⊂the␈α⊃generation␈α⊂of␈α⊂a␈α⊃computational␈α⊂specification␈α⊃of␈α⊂a
␈↓ α∧␈↓problem␈α
or␈α
task␈α
from␈α
a␈α∞descriptive␈α
specification.␈α
 We␈α
do␈α
not␈α
have␈α∞the␈α
redundancy
␈↓ α∧␈↓*******bletch***␈α⊂reword␈α⊂this␈α⊂mess␈α⊂*****␈α⊂of␈α⊂two␈α⊂specifications,␈α⊃one␈α⊂descriptive
␈↓ α∧␈↓and␈α
one␈α
computational,␈α
both␈α
written␈α
by␈α
the␈α
programmer,␈α
but␈α
we␈α
feel␈α
that␈α∞since,␈α
in
␈↓ α∧␈↓practice,␈α∞one␈α∞is␈α∂derived␈α∞from␈α∞the␈α∞other,␈α∂the␈α∞descriptive␈α∞specification,␈α∞being␈α∂free␈α∞of
␈↓ α∧␈↓computational␈α∃details␈α∃and␈α∃thus␈α∃less␈α∀prone␈α∃to␈α∃error,␈α∃is␈α∃the␈α∃appropriate␈α∀choice.
␈↓ α∧␈↓Several approaches to program synthesis are currently being investigated.

␈↓ α∧␈↓␈↓ αdWith␈α∞the␈α∂deductive␈α∞approach␈α∞(7,␈α∂8,␈α∞12,␈α∞14,␈α∂15,␈α∞18,␈α∞33,␈α∂34),␈α∞the␈α∂computer␈α∞is
␈↓ α∧␈↓given␈α≠specific␈α~rules␈α≠by␈α~which␈α≠it␈α~can␈α≠rewrite␈α~statements␈α≠syntactically␈α~while
␈↓ α∧␈↓maintaining␈α
equivalent␈α
meaning.␈α
 This␈α
kind␈α
of␈α
program␈α
synthesis␈α
is␈α
closely␈α
related



␈↓ α∧␈↓to␈α↔program␈α↔transformation␈α↔(4,␈α⊗9,␈α↔10,␈α↔16,␈α↔21,␈α⊗32).␈α↔The␈α↔intent␈α↔of␈α↔a␈α⊗program
␈↓ α∧␈↓transformation␈αsystem␈αis␈αto␈αmake␈αthe␈αgiven␈αprogram␈αmore␈αefficient␈αwhile␈αpreserving
␈↓ α∧␈↓its meaning.

␈↓ α∧␈↓␈↓ αdLess␈α∞formal␈α
techniques␈α∞have␈α
also␈α∞found␈α
favor.␈α∞ Natural␈α∞language␈α
dialogues
␈↓ α∧␈↓have␈αbeen␈αused␈αto␈αdescribe␈αa␈αproblem␈αto␈αthe␈αcomputer␈α(3,␈α22,␈α26,␈α31,␈α39).␈α The␈αuser
␈↓ α∧␈↓of␈α∞this␈α∞kind␈α
of␈α∞system␈α∞specifies␈α
the␈α∞task␈α∞at␈α
a␈α∞general␈α∞level,␈α
filling␈α∞in␈α∞the␈α∞details␈α
as
␈↓ α∧␈↓requested␈αby␈αthe␈αcomputer.␈α Still␈αother␈αapproaches␈αemploy␈αspecification␈αby␈αexample.
␈↓ α∧␈↓Some␈α∞systems␈α∂synthesize␈α∞programs␈α∂from␈α∞sample␈α∞input-output␈α∂pairs␈α∞(25,␈α∂38),␈α∞others
␈↓ α∧␈↓provide␈αsample␈αexecution␈α
traces␈α(6)␈αor␈α
even␈αanalogous␈αprograms␈α
(40).␈α Several␈αof␈α
the
␈↓ α∧␈↓approaches␈α
mentioned␈α
above␈α
are␈α
combined␈αin␈α
the␈α
PSI␈α
program␈α
synthesis␈α
system␈αat
␈↓ α∧␈↓Stanford University (24).

␈↓ α∧␈↓␈↓ αdEach␈αof␈α
the␈αtechniques␈α
mentioned␈αabove␈αhas␈α
been␈αinvestigated␈α
as␈αa␈αmeans␈α
to
␈↓ α∧␈↓synthesize␈α
programs␈αin␈α
a␈α
specific␈αtarget␈α
language.␈α It␈α
is␈α
our␈αthesis␈α
that␈αthe␈α
generation
␈↓ α∧␈↓of␈α⊗an␈α⊗algorithm␈α∃is␈α⊗a␈α⊗target-language-independent␈α∃process,␈α⊗and␈α⊗a␈α⊗system␈α∃that
␈↓ α∧␈↓generates␈α⊂programs␈α∂from␈α⊂their␈α∂specifications␈α⊂is␈α⊂a␈α∂valid␈α⊂and␈α∂viable␈α⊂way␈α⊂to␈α∂obtain
␈↓ α∧␈↓correct programs.

␈↓ α∧␈↓␈↓ αdWe␈α≡have␈α≡implemented␈α≥a␈α≡system␈α≡to␈α≥generate␈α≡programs␈α≡from␈α≥logic
␈↓ α∧␈↓specifications.␈α⊂ ******␈α⊂yuk␈α⊂*****␈α⊂The␈α⊂specifications␈α⊂are␈α⊂first␈α⊂translated␈α⊂into␈α⊂an
␈↓ α∧␈↓intermediate␈αlanguage␈αand␈αthen␈αa␈αprogram␈αis␈αgenerated␈αfrom␈αthe␈αintermediate␈αform.
␈↓ α∧␈↓Validity␈α
was␈α
established␈αby␈α
proving␈α
that␈α
the␈αtop␈α
level␈α
mappings␈α
from␈αspecification
␈↓ α∧␈↓to␈α
intermediate␈α
language␈α
to␈αtarget␈α
program␈α
(the␈α
proof␈αis␈α
for␈α
the␈α
mapping␈α
to␈αLISP)
␈↓ α∧␈↓are correct.

␈↓ α∧␈↓␈↓ αd We␈α∩drop␈α∩the␈α∩word␈α∩"synthesis"␈α∩and␈α∩use␈α∩program␈α∩"generation"␈α∪instead␈α∩to
␈↓ α∧␈↓avoid␈α
any␈αmisunderstanding␈α
of␈α
the␈αclaims␈α
being␈αmade.␈α
 The␈α
specification␈αlanguage
␈↓ α∧␈↓for␈α∞this␈α∞system␈α∞includes␈α∞a␈α∞subset␈α∞of␈α∞first-order␈α∞Predicate␈α∞Calculus␈α∞known␈α∞as␈α∞Horn
␈↓ α∧␈↓Clauses.␈α
 The␈α
specifications␈α
we␈α
require␈αare␈α
"descriptive"␈α
in␈α
that␈α
they␈α
specify␈αthe␈α
logic
␈↓ α∧␈↓of␈α∂the␈α∂program␈α∂without␈α∂specifying␈α∂an␈α∞implementation,␈α∂ but␈α∂they␈α∂are␈α∂also,␈α∂in␈α∞part,
␈↓ α∧␈↓"computational"␈α∪in␈α∪that␈α∪the␈α∪Horn␈α∪clauses␈α∪could␈α∪be␈α∪"run"␈α∪as␈α∪programs␈α∪given␈α∩a
␈↓ α∧␈↓complete theorem prover, or logic interpreter (2, 19, 29).

␈↓ α∧␈↓␈↓ αd*****hmmmmm*****␈α≥In␈α≤the␈α≥dissertation␈α≤we␈α≥formally␈α≥describe␈α≤the
␈↓ α∧␈↓specification␈αlanguage␈αvia␈α
a␈αcontext-free␈αgrammar␈αfor␈α
the␈αsyntax␈αand␈α
an␈αaxiomatic
␈↓ α∧␈↓description␈α∀of␈α∀the␈α∀semantics.␈α∀ Motivation␈α∀for␈α∀requiring␈α∀particular␈α∀items␈α∀in␈α∪the
␈↓ α∧␈↓specification␈α∂is␈α⊂provided␈α∂as␈α⊂well.␈α∂ We␈α⊂then␈α∂describe␈α⊂the␈α∂intermediate␈α⊂language␈α∂in
␈↓ α∧␈↓detail,␈α∂again␈α⊂supplying␈α∂a␈α∂context-free␈α⊂grammar␈α∂for␈α∂the␈α⊂syntax␈α∂and␈α⊂the␈α∂axiomatic
␈↓ α∧␈↓semantics.␈α⊂ The␈α⊂mapping␈α⊂from␈α⊂specification␈α⊂language␈α⊂to␈α⊂intermediate␈α⊂language␈α⊂is
␈↓ α∧␈↓given␈α∂by␈α∂means␈α∂of␈α∂a␈α∂function␈α∂␈↓I␈↓,␈α∂for␈α∂␈↓αinternalize␈↓,␈α∂and␈α∂we␈α∂prove␈α∂that␈α∂this␈α∂mapping
␈↓ α∧␈↓preserves␈α⊂the␈α⊃axiomatic␈α⊂semantics␈α⊃of␈α⊂the␈α⊃specifications.␈α⊂ We␈α⊃then␈α⊂prove␈α⊃that␈α⊂the
␈↓ α∧␈↓semantics␈α∞is␈α∂again␈α∞preserved␈α∞by␈α∂the␈α∞translation␈α∞from␈α∂the␈α∞intermediate␈α∂language␈α∞to
␈↓ α∧␈↓LISP.␈α We␈αdemonstrate␈αhow␈αto␈αextend␈αthe␈αsystem␈αto␈αhandle␈αgeneration␈αof␈αprograms
␈↓ α∧␈↓in␈αadditional␈α
languages.␈α The␈αadditions␈α
required␈αfor␈αeach␈α
new␈αlanguage␈αare␈α
referred
␈↓ α∧␈↓to␈α∂as␈α∞a␈α∂"back␈α∞end"␈α∂for␈α∂that␈α∞language.␈α∂ The␈α∞implementation␈α∂of␈α∞the␈α∂"back␈α∂end"␈α∞for
␈↓ α∧␈↓LISP␈α∀and␈α∀that␈α∀for␈α∪Pascal␈α∀are␈α∀also␈α∀discussed.␈α∪ We␈α∀include␈α∀some␈α∀notes␈α∀on␈α∪the



␈↓ α∧␈↓implementation␈αand␈αthen␈αdiscuss␈αthe␈αconclusions␈αthat␈αcan␈αbe␈αdrawn␈αfrom␈αthis␈αeffort,
␈↓ α∧␈↓as well as topics of further research that were suggested by the project.

␈↓ α∧␈↓␈↓ αd*****ditto*****␈α∂The␈α∞system␈α∂described␈α∞is␈α∂unique␈α∞in␈α∂its␈α∞ability␈α∂to␈α∞generate
␈↓ α∧␈↓programs␈α→in␈α→more␈α_than␈α→one␈α→language.␈α_The␈α→system␈α→represents␈α→a␈α_non-trivial
␈↓ α∧␈↓application␈α⊃of␈α∩formal␈α⊃techniques,␈α⊃ generating␈α∩a␈α⊃version␈α⊃of␈α∩itself␈α⊃from␈α∩its␈α⊃formal
␈↓ α∧␈↓specification.␈α  Given␈αthe␈α"back␈αend"␈αdescribing␈αa␈αparticular␈αtarget␈αlanguage,␈αwe␈αcan
␈↓ α∧␈↓generate␈α⊂the␈α∂system␈α⊂itself␈α⊂in␈α∂the␈α⊂language,␈α⊂making␈α∂it␈α⊂immediately␈α⊂portable.␈α∂ Most
␈↓ α∧␈↓importantly,␈αit␈αprovides␈αa␈αmeans␈αof␈αobtaining␈αcorrect␈αprograms␈αthat␈αis␈αdecidedly␈αless
␈↓ α∧␈↓painful␈α∀than␈α∪verification.␈α∀ The␈α∪user␈α∀is␈α∪still␈α∀required␈α∪to␈α∀specify␈α∪the␈α∀logic␈α∀of␈α∪a
␈↓ α∧␈↓program,␈αbut␈αthe␈αlanguage␈αused␈αin␈αthe␈αspecification␈αfrees␈αthe␈αuser␈αfrom␈α
concerns␈αof
␈↓ α∧␈↓representation and implementation.

␈↓"∧␈↓ α∧␈↓␈↓ ¬␈↓↓Specification Language␈↓

␈↓"∀␈↓ α∧␈↓␈↓ αdThe␈α⊂input␈α⊂to␈α⊂the␈α∂system␈α⊂is␈α⊂a␈α⊂sequence␈α∂of␈α⊂definitions.␈α⊂ A␈α⊂target␈α∂definition
␈↓ α∧␈↓simply␈αindicates␈αthe␈α
target␈αlanguage␈αto␈α
be␈αused.␈α   The␈α
other␈αkinds␈αof␈αdefinitions␈α
are
␈↓ α∧␈↓function, type and generic.

␈↓ α∧␈↓␈↓ αdA␈α∩function␈α⊃definition␈α∩has␈α⊃six␈α∩parts,␈α∩a␈α⊃name,␈α∩an␈α⊃input␈α∩pattern,␈α∩a␈α⊃formal
␈↓ α∧␈↓parameter list, a precondition, a postcondition, and a body.
␈↓ α∧␈↓For example:
␈↓ α∧␈↓␈↓ αd                        ␈↓αfunction Fact
␈↓ α∧␈↓α␈↓ αd                        ␈↓↓input pattern? ␈↓α(1 0)␈↓↓
␈↓ α∧␈↓↓␈↓ αd                        parameter list? ␈↓α(x y)␈↓↓
␈↓ α∧␈↓↓␈↓ αd                        precond? ␈↓αInteger(x, true) ∧ ≥(x, 0, true).␈↓↓
␈↓ α∧␈↓↓␈↓ αd                        postcond? ␈↓αInteger(y, true) ∧ >(y, 0, true).␈↓↓
␈↓ α∧␈↓↓␈↓ αd                        body? ␈↓αFact(0, 1)
␈↓ α∧␈↓α␈↓ αd                               Fact(z, w) ← Sub1(z, z1), Fact(z1, w1), *(z, w1, w).␈↓

␈↓ α∧␈↓where␈αonly␈αthe␈αitalicized␈αinformation␈αis␈αsupplied␈αby␈αthe␈αuser.␈α An␈αinput␈αpattern␈αis␈αa
␈↓ α∧␈↓list␈α
of␈α
1's␈α
and␈α
0's␈α
indicating␈α
which␈α
of␈α
the␈α
arguments␈α
of␈α
the␈α
function␈α
being␈αdefined
␈↓ α∧␈↓are␈α⊂expected␈α⊂to␈α⊂hold␈α⊂input␈α⊂values␈α∂and␈α⊂which␈α⊂are␈α⊂used␈α⊂to␈α⊂carry␈α⊂values␈α∂produced
␈↓ α∧␈↓during the computation of the function, respectively.

␈↓ α∧␈↓␈↓ αdA␈α
formal␈α
parameter␈α
list␈α
is␈α
required␈α
to␈α
match␈α
up␈α
the␈α
appropriate␈αarguments
␈↓ α∧␈↓for the precondition and postcondition specifications.

␈↓ α∧␈↓␈↓ αdThe␈αprecondition␈αis␈αa␈α
well-formed-formula␈αof␈αpredicate␈αcalculus,␈α defined␈α
on
␈↓ α∧␈↓the␈α⊃input␈α⊃variables,␈α⊃that␈α⊃is␈α⊃true␈α⊃only␈α⊃if␈α⊃the␈α⊃function␈α⊃is␈α⊃defined␈α⊃for␈α∩those␈α⊃input
␈↓ α∧␈↓variables.␈α⊂ By␈α⊂precisely␈α⊂specifying␈α⊂ the␈α∂domain␈α⊂of␈α⊂the␈α⊂function␈α⊂we␈α⊂can␈α∂guarantee
␈↓ α∧␈↓termination␈α
of␈α
the␈α
program.␈α
 Similarly,␈α
the␈α
postcondition␈α
is␈α
a␈α
predicate␈α
formula␈α
on
␈↓ α∧␈↓the␈α⊂output␈α⊂variables␈α⊂that␈α⊂specifies␈α⊃the␈α⊂range␈α⊂of␈α⊂the␈α⊂output.␈α⊂ Taken␈α⊃together,␈α⊂the
␈↓ α∧␈↓precondition␈α
and␈α
postcondition␈α
specify␈α
the␈αfunctionality,␈α
i.e.␈α
the␈α
domain␈α
and␈αrange,
␈↓ α∧␈↓of␈α⊂the␈α∂program␈α⊂being␈α∂defined.␈α⊂ The␈α∂range␈α⊂given␈α∂may␈α⊂in␈α∂fact␈α⊂be␈α∂larger␈α⊂than␈α∂the
␈↓ α∧␈↓actual␈αrange␈αof␈αthe␈αfunction,␈αbut␈αthe␈αdomain␈αgiven␈αmust␈αnot␈αinclude␈αany␈αextraneous
␈↓ α∧␈↓elements.



␈↓ α∧␈↓␈↓ αdA␈α∞body␈α∞definition␈α
is␈α∞a␈α∞set␈α
of␈α∞Horn␈α∞clauses␈α
(29)␈α∞that␈α∞describes␈α∞the␈α
function,
␈↓ α∧␈↓usually␈α
recursively,␈αin␈α
an␈α
axiomatic␈αway.␈α
 Each␈α
Horn␈αclause␈α
is␈α
an␈αimplication,␈α
stating
␈↓ α∧␈↓that␈α
a␈α
goal␈α(the␈α
consequent)␈α
can␈α
be␈αasserted␈α
if␈α
the␈α
conjunction␈αof␈α
a␈α
set␈α
of␈αsubgoals
␈↓ α∧␈↓(the␈αantecedent)␈αis␈αsatisfied.␈α In␈αwriting␈αa␈αbody␈αdefinition␈αwe␈αare␈αasserting␈αthat␈αeach
␈↓ α∧␈↓of␈αthese␈αimplications␈αis␈αtrue;␈αthat␈αis,␈αeach␈αmay␈αbe␈αconsidered␈αan␈αaxiom␈αand␈αbe␈αused
␈↓ α∧␈↓in deriving theorems.

␈↓ α∧␈↓␈↓ αdIf␈α⊃the␈α⊃antecedent␈α⊃of␈α⊃an␈α⊃implication␈α⊂is␈α⊃empty,␈α⊃the␈α⊃clause␈α⊃is␈α⊃considered␈α⊂an
␈↓ α∧␈↓assertion␈α∂and␈α∂we␈α∂do␈α∞not␈α∂write␈α∂the␈α∂arrow,␈α∞as␈α∂in␈α∂␈↓αFact(0,␈α∂1)␈↓␈α∞(read␈α∂"Fact␈α∂of␈α∂0␈α∂is␈α∞1").
␈↓ α∧␈↓Kowalski␈α∃(29)␈α∃describes␈α∀the␈α∃interpretation␈α∃of␈α∀Horn␈α∃clauses␈α∃as␈α∃a␈α∀programming
␈↓ α∧␈↓language.

␈↓ α∧␈↓␈↓ αdA␈αtype␈αdefinition␈αis␈αa␈αdefinition␈αof␈αa␈αfunction␈αthat␈αrecognizes␈αoccurrences␈αof
␈↓ α∧␈↓the␈α∞type.␈α∞A␈α∞generic␈α∞function␈α∞is␈α∞one␈α
in␈α∞which␈α∞the␈α∞input␈α∞pattern␈α∞is␈α∞allowed␈α∞to␈α
vary.
␈↓ α∧␈↓For␈αexample,␈αone␈α
might␈αwish␈αto␈α
define␈αa␈αfunction␈α
"␈↓αTimes(x,␈αy,␈αz)␈↓",␈α
meaning␈α"␈α␈↓αx␈↓␈α
times
␈↓ α∧␈↓␈↓αy␈↓␈α∩is␈α∪␈↓αz␈↓".␈α∩ If␈α∪defined␈α∩as␈α∪a␈α∩generic␈α∪function␈α∩we␈α∪can␈α∩use␈α∪␈↓αTimes␈↓␈α∩in␈α∪defining␈α∩other
␈↓ α∧␈↓functions␈α
whenever␈αwe␈α
have␈αtwo␈α
of␈αits␈α
arguments␈αavailable␈α
and␈αwish␈α
to␈αcompute␈α
the
␈↓ α∧␈↓third.

␈↓ α∧␈↓␈↓ αdA␈α⊃generic␈α∩definition␈α⊃includes␈α⊃its␈α∩name,␈α⊃a␈α⊃formal␈α∩parameter␈α⊃list,␈α⊃a␈α∩list␈α⊃of
␈↓ α∧␈↓choices␈αspecifying␈αhow␈αthe␈αfunction␈αmay␈αbe␈αused,␈αand␈αone␈αor␈αmore␈αbody␈αdefinitions.
␈↓ α∧␈↓With␈αHorn␈αClauses,␈αit␈αis␈α
often␈αthe␈αcase␈αthat␈αone␈α
description␈αof␈αthe␈αbody␈αcan␈αbe␈α
used
␈↓ α∧␈↓for␈α
several␈α∞calling␈α
styles␈α∞(36).␈α
 A␈α∞choice␈α
consists␈α∞of␈α
an␈α∞input␈α
pattern,␈α∞a␈α
name␈α∞to␈α
be
␈↓ α∧␈↓associated␈α∀with␈α∀this␈α∀particular␈α∀style␈α∀of␈α∀call␈α∀on␈α∀the␈α∀function,␈α∀a␈α∀precondition,␈α∀a
␈↓ α∧␈↓postcondition,␈α∞and␈α
a␈α∞body␈α
name␈α∞indicating␈α
the␈α∞function␈α
body␈α∞to␈α
be␈α∞used.␈α∞ A␈α
body
␈↓ α∧␈↓definition associates a body name with a definition (i.e. a set of Horn clauses).

␈↓ α∧␈↓␈↓ αdThe␈α
semantics␈α
of␈αa␈α
function␈α
specification,␈α
informally,␈αis␈α
that␈α
for␈α
all␈αpossible
␈↓ α∧␈↓instantiations␈αof␈αthe␈αformal␈αparameter␈αlist,␈αif␈αeach␈αparameter␈αdesignated␈αas␈αan␈αinput
␈↓ α∧␈↓by␈α∂the␈α⊂input␈α∂pattern␈α⊂has␈α∂a␈α∂value␈α⊂bound␈α∂to␈α⊂it␈α∂and␈α∂the␈α⊂value␈α∂of␈α⊂the␈α∂precondition
␈↓ α∧␈↓evaluated␈αon␈αthe␈α
inputs␈αis␈αtrue␈α
(i.e.,␈αthe␈αinputs␈α
lie␈αwithin␈αthe␈α
domain␈αof␈αdefinition␈α
of
␈↓ α∧␈↓the␈α
function),␈α∞then␈α
the␈α∞conjunction␈α
 of␈α
the␈α∞Horn␈α
clauses␈α∞and␈α
the␈α∞postcondition␈α
are
␈↓ α∧␈↓true.  A formal statement is given in the dissertation.
␈↓ α∧␈↓Our ␈↓αFact␈↓ example has the semantics of the associated first order logic expression:
␈↓ α∧␈↓␈↓ αd␈↓↓∀x,y [ defined[(x)] ∧ Integer(x, true) ∧ ≥(x, 0, true)   →
␈↓ α∧␈↓↓␈↓ αd        Fact(0, 1)
␈↓ α∧␈↓↓␈↓ αd          ∧  ∀z,z1,w,w1 [ [Sub1(z, z1) ∧ Fact(z1, w1) ∧ *(z, w1, w)  →  Fact(z, w)] ]
␈↓ α∧␈↓↓␈↓ αd               ∧ [ Fact(x, y)   → Integer(y, true) ∧ >(y, 0, true) ]  ]

␈↓ α∧␈↓The semantics of a type specification is similar.

␈↓ α∧␈↓␈↓ αdThe␈α_generic␈α_specification␈α_has␈α_the␈α_effect␈α_of␈α_defining␈α_several␈α_different
␈↓ α∧␈↓functions␈α∂and␈α∂associating␈α∂them␈α⊂all␈α∂with␈α∂a␈α∂"generic"␈α⊂name␈α∂that␈α∂can␈α∂be␈α⊂used␈α∂when
␈↓ α∧␈↓specifying␈α∀other␈α∃functions␈α∀rather␈α∀than␈α∃using␈α∀a␈α∀different␈α∃name␈α∀every␈α∃time␈α∀the
␈↓ α∧␈↓function is used in a different way, that is, with a different input-pattern.



␈↓ α∧␈↓␈↓ ¬∂␈↓↓Intermediate Language␈↓

␈↓"∀␈↓ α∧␈↓␈↓ αdThe␈αintermediate␈αlanguage␈αform␈αof␈αfunction␈αdefinitions␈αis␈αonly␈αused␈αinternal
␈↓ α∧␈↓to␈α_the␈α_system.␈α↔ The␈α_auxiliary␈α_specifications␈α↔(all␈α_but␈α_body␈α_specifications)␈α↔are
␈↓ α∧␈↓essentially␈α
unchanged;␈α
their␈α
representation␈α
is␈αslightly␈α
different␈α
but␈α
exactly␈α
the␈αsame
␈↓ α∧␈↓information␈α
is␈α
expressed.␈α Thus,␈α
the␈α
interesting␈αpart␈α
of␈α
the␈αintermediate␈α
form␈α
is␈αits
␈↓ α∧␈↓treatment of the body specification.

␈↓ α∧␈↓␈↓ αdThe␈α∩body␈α⊃of␈α∩a␈α∩function␈α⊃in␈α∩internal␈α⊃form␈α∩is␈α∩a␈α⊃"backtracking-conditional"
␈↓ α∧␈↓("bktrkcond"␈α→for␈α→short).␈α→ Each␈α→clause␈α_of␈α→the␈α→body␈α→specification␈α→becomes␈α_an
␈↓ α∧␈↓"alternative"␈αin␈αthe␈αbktrkcond.␈α An␈αalternative␈αconsists␈αof␈αa␈α"match"-part,␈αthat␈αis␈αan
␈↓ α∧␈↓argument␈αlist␈α
to␈αbe␈α
matched␈αagainst␈α
the␈αactual␈αparameters␈α
of␈αa␈α
function␈αcall,␈α
and␈αa
␈↓ α∧␈↓"try"␈αpart␈αconsisting␈αof␈αthe␈αsubgoals␈αto␈αbe␈αaccomplished.␈α The␈αbacktracking␈αinvolved
␈↓ α∧␈↓is␈α∂well-behaved␈α⊂since␈α∂we␈α⊂may␈α∂backtrack␈α⊂only␈α∂over␈α⊂entire␈α∂alternatives,␈α⊂never␈α∂over
␈↓ α∧␈↓individual␈α⊃subgoals␈α⊃in␈α⊃the␈α⊃try-part␈α⊃of␈α⊃an␈α⊃alternative.␈α⊃ All␈α⊃that␈α⊃may␈α⊃have␈α⊃to␈α⊂be
␈↓ α∧␈↓undone␈α∀are␈α∀the␈α∪bindings␈α∀made␈α∀in␈α∀accomplishing␈α∪the␈α∀unification␈α∀of␈α∀the␈α∪actual
␈↓ α∧␈↓parameter␈α⊃list␈α⊃with␈α∩the␈α⊃argument␈α⊃list␈α⊃in␈α∩the␈α⊃match-part␈α⊃of␈α⊃the␈α∩alternative.␈α⊃ We
␈↓ α∧␈↓impose␈αdeterminism␈α
on␈αthe␈αprogram␈α
at␈αthis␈α
stage␈αby␈αinsisting␈α
on␈αa␈α
particular␈αorder
␈↓ α∧␈↓for considering the alternatives.

␈↓ α∧␈↓␈↓ αdThe␈αintermediate␈αform␈αof␈αa␈αgeneric␈αdefinition␈αcontains␈αthe␈αgeneric␈αname,␈αthe
␈↓ α∧␈↓formal␈α
parameter␈αlist,␈α
and␈α
a␈αlist␈α
associating␈α
input-patterns␈αwith␈α
the␈α
function␈αname␈α
to
␈↓ α∧␈↓be␈α∂used␈α∂when␈α∂that␈α∂input-pattern␈α∂is␈α∂recognized.␈α∂A␈α∂generic␈α∂specification␈α⊂causes␈α∂the
␈↓ α∧␈↓function␈α∞definitions␈α∞for␈α∞each␈α∂alternative␈α∞version␈α∞of␈α∞the␈α∂function␈α∞to␈α∞be␈α∞made,␈α∂as␈α∞if
␈↓ α∧␈↓they had each been specified separately.

␈↓ α∧␈↓␈↓ αdThe␈α⊗syntax␈α⊗and␈α⊗semantics␈α⊗of␈α⊗the␈α⊗Intermediate␈α⊗Language␈α↔are␈α⊗formally
␈↓ α∧␈↓described␈α⊂in␈α⊂the␈α⊂dissertation.␈α⊂ The␈α⊃specification␈α⊂of␈α⊂the␈α⊂factorial␈α⊂function␈α⊃has␈α⊂the
␈↓ α∧␈↓following form in the Intermediate Language:
␈↓ α∧␈↓α␈↓ αd                (function Fact (1 0) (!x !y)
␈↓ α∧␈↓α␈↓ αd                        (∧ (Integer !x true) (≥ !x 0 true))
␈↓ α∧␈↓α␈↓ αd                        (∧ (Integer !y true) (> !y 0 true))
␈↓ α∧␈↓α␈↓ αd                        (bktrkcond ((0 1) (try))
␈↓ α∧␈↓α␈↓ αd                                   ((!z !w) (try (Sub1 !z !z1)
␈↓ α∧␈↓α␈↓ αd                                                 (Fact !z1 !w1)
␈↓ α∧␈↓α␈↓ αd                                                 (* !z !w1 !w)  ) )
␈↓ α∧␈↓α␈↓ αd                          ) )

␈↓"∧␈↓ α∧␈↓␈↓ βZ␈↓↓Correctness of the Mapping to Intermediate Form␈↓

␈↓"∀␈↓ α∧␈↓␈↓ αdWe␈α∃ show␈α∃that␈α∃the␈α∃semantics␈α∀of␈α∃an␈α∃input␈α∃specification␈α∃is␈α∀"sufficiently"
␈↓ α∧␈↓preserved␈αin␈αthe␈αmapping␈αto␈αintermediate␈αform.␈α By␈α"sufficiently"␈αwe␈αmean␈αthat␈αthe
␈↓ α∧␈↓semantics␈α∪of␈α∀the␈α∪intermediate␈α∀form␈α∪of␈α∪a␈α∀function␈α∪definition␈α∀is␈α∪implied␈α∀by␈α∪the
␈↓ α∧␈↓semantics␈αof␈αthe␈αinput␈αspecification,␈α
and␈αfurthermore,␈αif␈αevery␈α function␈α(or␈α
type)␈α␈↓αP␈↓
␈↓ α∧␈↓is␈α
defined␈α∞such␈α
that␈α∞for␈α
each␈α∞input␈α
tuple,␈α∞␈↓∂¬␈↓αx␈↓βi␈↓,␈α
(i.e.,␈α∞tuple␈α
with␈α∞which␈α
the␈α∞function␈α
is



␈↓ α∧␈↓called)␈αthere␈αexists␈αa␈αunique␈αoutput␈αtuple,␈α␈↓∂¬␈↓αx␈↓βo␈↓,␈αsuch␈αthat␈α␈↓αP(␈↓∂¬␈↓αx␈↓βo␈↓α)␈↓␈αis␈αderivable␈αusing␈αthe
␈↓ α∧␈↓input␈α
semantics,␈α
then␈α
␈↓αP(␈↓∂¬␈↓αx␈↓βo␈↓α)␈↓␈α
is␈αderivable␈α
using␈α
the␈α
semantics␈α
of␈α
the␈αintermediate␈α
form
␈↓ α∧␈↓of␈α the␈αdefinition.␈α We␈αrefer␈αto␈αthis␈αrestriction␈αof␈αrequiring␈αuniqueness␈αof␈αthe␈αoutput
␈↓ α∧␈↓tuple by saying that we are defining only "functional" relationships.

␈↓ α∧␈↓␈↓ αdThe␈α⊂semantics␈α⊂of␈α∂input␈α⊂and␈α⊂internal␈α⊂form␈α∂are␈α⊂not␈α⊂equivalent␈α⊂because␈α∂the
␈↓ α∧␈↓input␈α∂semantics␈α∞may␈α∂be␈α∞used␈α∂several␈α∞ways␈α∂to␈α∞generate␈α∂proofs.␈α∞ This␈α∂is␈α∞due␈α∂to␈α∞the
␈↓ α∧␈↓nondeterministic␈α
nature␈α∞of␈α
the␈α
process␈α∞of␈α
finding␈α∞proofs.␈α
 At␈α
any␈α∞stage␈α
of␈α∞a␈α
proof,
␈↓ α∧␈↓there␈αmay␈αbe␈αmany␈αHorn␈αclauses␈αthat␈αare␈αapplicable␈αas␈αaxioms,␈αand␈αdifferent␈αproof
␈↓ α∧␈↓paths␈α∪may␈α∪generate␈α∪different␈α∪results.␈α∩ However,␈α∪we␈α∪have␈α∪restricted␈α∪ourselves␈α∩to
␈↓ α∧␈↓defining␈αfunctional␈α
relationships␈αrather␈α
than␈αthe␈α
more␈αgeneral␈α
"relations"␈αwhich␈α
may
␈↓ α∧␈↓be␈αone-to-many␈αmappings.␈α Thus,␈αno␈αmatter␈αwhat␈αdirection␈αthe␈αproof␈αtakes,␈αthere␈αis
␈↓ α∧␈↓a unique result.

␈↓ α∧␈↓␈↓ αd  In␈α⊂the␈α⊂intermediate␈α⊃form␈α⊂we␈α⊂are␈α⊂forced␈α⊃to␈α⊂attempt␈α⊂the␈α⊂alternatives␈α⊃in␈α⊂a
␈↓ α∧␈↓specific␈α
order.␈α Due␈α
to␈α
the␈αdeterminism␈α
introduced␈α
we␈αwill␈α
follow␈α
precisely␈αone␈α
proof,
␈↓ α∧␈↓the␈α
same␈α
proof,␈α
every␈α∞time␈α
a␈α
procedure␈α
is␈α
called␈α∞with␈α
the␈α
same␈α
input␈α∞values.␈α
 The
␈↓ α∧␈↓important␈αpoint␈αto␈αestablish␈αis␈αthat␈αwhenever␈αa␈αunique␈αanswer␈αmay␈αbe␈αfound␈αin␈αthe
␈↓ α∧␈↓nondeterministic␈αproof␈αprocess,␈αour␈αdeterministic␈αsearch␈αwill␈αfind␈αit␈αas␈αwell.␈α This␈αis
␈↓ α∧␈↓proved formally in the dissertation.

␈↓"∧␈↓ α∧␈↓␈↓ ∧F␈↓↓Conclusions and Further Research␈↓

␈↓"∀␈↓ α∧␈↓␈↓ αdWe␈α
have␈αshown,␈α
through␈αproofs␈α
of␈αthe␈α
correctness␈αof␈α
the␈αmappings␈α
involved,
␈↓ α∧␈↓that␈α⊂the␈α⊂system␈α⊂described␈α⊂in␈α⊃the␈α⊂dissertation␈α⊂provides␈α⊂a␈α⊂valid␈α⊂way␈α⊃of␈α⊂generating
␈↓ α∧␈↓correct␈αprograms.␈α The␈αuser␈αis␈αstill␈αleft␈αwith␈αthe␈αtask␈αof␈αinventing␈αthe␈αcomputational
␈↓ α∧␈↓logic␈α∂description␈α∂of␈α∂the␈α∂program␈α∂desired.␈α∂ We␈α∂feel␈α∂that␈α∂this␈α∂is␈α∂reasonable␈α⊂and␈α∂an
␈↓ α∧␈↓advance␈α
in␈α
the␈α
process␈α
of␈α
obtaining␈α
a␈α
correct␈α
program␈α
since␈α
the␈α
programmer␈α
is␈α
no
␈↓ α∧␈↓longer burdened with the problems of representation and implementation.

␈↓ α∧␈↓␈↓ αdThe␈α_system␈α_is␈α↔"reasonably"␈α_target-language-independent,␈α_qualified␈α↔only
␈↓ α∧␈↓because␈α∩it␈α∩is␈α∩easier␈α⊃to␈α∩translate␈α∩to␈α∩some␈α∩languages␈α⊃than␈α∩to␈α∩others.␈α∩ For␈α∩ease␈α⊃of
␈↓ α∧␈↓translation,␈αthe␈αtarget␈α
language␈αshould␈αallow␈α
recursion.␈α The␈α"back-end"␈αnecessary␈α
to
␈↓ α∧␈↓translate␈α⊂to␈α⊂a␈α∂non-recursive␈α⊂language,␈α⊂although␈α∂certainly␈α⊂feasible,␈α⊂would␈α⊂be␈α∂more
␈↓ α∧␈↓complicated␈α
than␈αthat␈α
for␈αa␈α
language␈αallowing␈α
recursion.␈α We␈α
feel␈αthis␈α
is␈α
almost␈αno
␈↓ α∧␈↓restriction␈α∀at␈α∪all␈α∀since␈α∀we␈α∪believe␈α∀that␈α∪recursion␈α∀is␈α∀important␈α∪enough␈α∀to␈α∀be␈α∪a
␈↓ α∧␈↓minimum requirement for any language to be considered "reasonable".

␈↓ α∧␈↓␈↓ αdThe␈αtype␈α
structure␈αof␈α
a␈αtarget␈α
language␈αis␈α
an␈αimportant␈α
factor␈αin␈α
determining
␈↓ α∧␈↓the␈αease␈αof␈αits␈αaddition␈αto␈αthe␈αsystem.␈α The␈αsimplest␈αlanguages␈αto␈αdeal␈αwith␈αare␈αthose
␈↓ α∧␈↓that␈α
are␈α
type-free,␈α
allowing␈α
type␈α
specifications␈α
to␈α
be␈α
translated␈α
into␈α
functions␈αthat␈α
are
␈↓ α∧␈↓recognizers␈αfor␈αthe␈αtype␈αbeing␈αdefined.␈αIn␈αa␈αtyped␈αlanguage,␈αone␈αoften␈αfeels␈αthe␈αneed
␈↓ α∧␈↓(or␈αdesire)␈αfor␈αpolymorphic␈αfunctions␈αas␈αallowed␈αby␈αLCF␈α(23).␈α A␈αsimple␈αexample␈αof
␈↓ α∧␈↓a␈αfunction␈αthat␈αis␈αby␈αnature␈αpolymorphic␈αis␈αa␈αsymbol␈αtable␈αlookup.␈α The␈αtype␈αof␈αthe
␈↓ α∧␈↓result␈α
of␈αa␈α
lookup␈α
should␈αagree␈α
with␈αthe␈α
type␈α
of␈αthe␈α
variable␈αthe␈α
function␈α
is␈αcalled
␈↓ α∧␈↓with.␈α However,␈αthere␈αmay␈αbe␈αseveral␈αdifferent␈αtypes␈αof␈αvariables␈αand␈αvalues␈α
in␈αthe



␈↓ α∧␈↓table␈α∞at␈α
any␈α∞time.␈α
 The␈α∞strong␈α∞typing␈α
of␈α∞Pascal␈α
complicated␈α∞its␈α∞implementation␈α
for
␈↓ α∧␈↓this␈α
system.␈α
In␈αthe␈α
dissertation␈α
we␈αdiscuss␈α
the␈α
implementations␈αof␈α
LISP␈α
and␈αPascal,
␈↓ α∧␈↓and describe how to add a new target language to the system.

␈↓ α∧␈↓␈↓ αdThe␈α⊃use␈α⊃of␈α⊃generic␈α⊃functions␈α⊃in␈α⊃the␈α⊃specifications␈α⊃is␈α⊃a␈α⊃feature␈α⊃making␈α⊂it
␈↓ α∧␈↓possible␈α↔to␈α↔synthesize␈α↔ several␈α↔programs␈α↔from␈α↔a␈α↔single␈α↔specification.␈α⊗ Generic
␈↓ α∧␈↓functions␈α
also␈α
provide␈αa␈α
convenient␈α
tool␈α
in␈αdefining␈α
other␈α
functions.␈α The␈α
portability
␈↓ α∧␈↓of␈α
the␈α
system␈α
is␈α
evidenced␈α
by␈α
its␈αability␈α
to␈α
generate␈α
a␈α
version␈α
of␈α
itself.␈α
 This␈αability␈α
is
␈↓ α∧␈↓also␈α∂an␈α∂indication␈α∂that␈α∂the␈α⊂system␈α∂can␈α∂handle␈α∂large␈α∂"practical"␈α⊂problems.␈α∂ Several
␈↓ α∧␈↓sample programs have been generated and are listed in the dissertation.

␈↓ α∧␈↓␈↓ αdExtensions␈α⊃to␈α⊂the␈α⊃system␈α⊂and␈α⊃subjects␈α⊂of␈α⊃further␈α⊂research␈α⊃have␈α⊂suggested
␈↓ α∧␈↓themselves␈α∂along␈α∂the␈α∂way.␈α⊂ We␈α∂would␈α∂like␈α∂to␈α∂add␈α⊂a␈α∂front-end␈α∂to␈α∂the␈α⊂system␈α∂that
␈↓ α∧␈↓would␈α
allow␈α
more␈α
natural␈α
input.␈α
 This␈α
includes␈α
several␈α
extensions␈α
of␈α
the␈α
syntax␈α
of
␈↓ α∧␈↓the␈α⊃specification␈α⊃language.␈α⊃ We␈α⊃can␈α⊃extend␈α⊃the␈α⊃syntax␈α⊃of␈α⊃Horn␈α⊃clauses␈α⊃to␈α⊃allow
␈↓ α∧␈↓mixed␈α∞conjunctions␈α∞and␈α∞disjunctions␈α∞of␈α∞positive␈α∞literals␈α∞on␈α∞the␈α∞right␈α∞hand␈α∂side␈α∞of
␈↓ α∧␈↓the arrow.

␈↓ α∧␈↓␈↓ αdIt␈α
would␈αbe␈α
nice␈αto␈α
allow␈αfull␈α
use␈α
of␈αPredicate␈α
Calculus␈αin␈α
the␈αspecification␈α
of
␈↓ α∧␈↓a␈α∂function.␈α∂ This␈α∂is␈α∂a␈α⊂much␈α∂more␈α∂difficult␈α∂problem.␈α∂ Synthesis␈α∂of␈α⊂programs␈α∂from
␈↓ α∧␈↓general␈αdescriptions␈αis␈αbeing␈αstudied␈αby␈αseveral␈αresearchers␈α(5,␈α11,␈α12,␈α13,␈α14,␈α15,␈α18,
␈↓ α∧␈↓33, 34).  Their results may be incorporated in this system in the future.

␈↓ α∧␈↓␈↓ αdWe␈α⊃would␈α⊂like␈α⊃to␈α⊂include␈α⊃an␈α⊂interactive␈α⊃environment␈α⊂that␈α⊃helps␈α⊃the␈α⊂user
␈↓ α∧␈↓derive␈α~the␈α~specifications␈α~for␈α~a␈α→program␈α~and␈α~prove␈α~the␈α~correctness␈α~of␈α→the
␈↓ α∧␈↓specifications.␈α∪The␈α∪system␈α∀could␈α∪check␈α∪the␈α∀completeness␈α∪of␈α∪the␈α∀specification␈α∪by
␈↓ α∧␈↓ensuring␈αthat␈αat␈αleast␈αone␈αHorn␈αclause␈αis␈αapplicable␈αto␈αevery␈αelement␈αof␈αthe␈αdomain
␈↓ α∧␈↓of␈αthe␈αfunction␈αas␈αspecified␈αby␈αthe␈αprecondition.␈α This␈αis␈αdifficult␈αin␈αgeneral␈αbut␈αfor
␈↓ α∧␈↓inductively␈αdefined␈αdomains␈αmay␈αsimply␈αbe␈αa␈αreminder␈αto␈αthe␈αprogrammer␈αthat␈α
they
␈↓ α∧␈↓include␈α
basis␈α
and␈α
constructed␈α
elements.␈α
 To␈α
prove␈α
the␈α
correctness␈α
of␈α
a␈αspecification
␈↓ α∧␈↓one␈αmust:␈α
1)Prove␈αeach␈αHorn␈α
clause␈αis␈αa␈α
theorem␈αin␈αthe␈α
problem␈αdomain;␈α
2)␈αProve
␈↓ α∧␈↓that␈α⊂the␈α∂precondition␈α⊂guarantees␈α⊂termination␈α∂of␈α⊂the␈α⊂program;␈α∂ and␈α⊂3)␈α⊂Prove␈α∂that
␈↓ α∧␈↓successful␈α⊃termination␈α⊂of␈α⊃the␈α⊃program␈α⊂always␈α⊃results␈α⊃in␈α⊂an␈α⊃answer␈α⊃satisfying␈α⊂the
␈↓ α∧␈↓postcondition,␈αand␈αthat␈αthe␈α
answer␈αproduced␈αis␈αunique.␈α It␈α
is␈αof␈αcourse␈αtoo␈α
much␈αto
␈↓ α∧␈↓expect␈α⊃that␈α⊃the␈α⊃system␈α⊃be␈α⊃capable␈α⊃of␈α⊃doing␈α⊃all␈α⊃of␈α⊃this␈α⊃on␈α⊃its␈α⊃own,␈α⊃but␈α⊃a␈α⊂semi-
␈↓ α∧␈↓automatic verifier or proof checker would be useful.

␈↓ α∧␈↓␈↓ αdThere␈α∞are␈α∂also␈α∞several␈α∞extensions␈α∂to␈α∞the␈α∞capabilities␈α∂of␈α∞the␈α∞system␈α∂that␈α∞are
␈↓ α∧␈↓desirable.␈α⊂ We␈α⊃would␈α⊂like␈α⊂to␈α⊃extend␈α⊂the␈α⊂use␈α⊃of␈α⊂generic␈α⊂function␈α⊃specifications␈α⊂to
␈↓ α∧␈↓allow␈α∞selection␈α∞of␈α∞individual␈α∞versions␈α∞of␈α∞the␈α∞function␈α∞by␈α∞type␈α∞of␈α∞the␈α∞arguments␈α∞as
␈↓ α∧␈↓well␈α⊃as␈α⊂by␈α⊃input␈α⊂pattern.␈α⊃ Another␈α⊂useful␈α⊃feature␈α⊂would␈α⊃be␈α⊂obtained␈α⊃by␈α⊂making
␈↓ α∧␈↓arrays a primitive data type.

␈↓ α∧␈↓␈↓ αdWe␈α↔would␈α⊗like␈α↔to␈α↔include␈α⊗a␈α↔way␈α↔of␈α⊗indicating␈α↔that␈α↔selective␈α⊗subgoal
␈↓ α∧␈↓backtracking␈α
is␈α
desired.␈α
 This␈αwould␈α
give␈α
us␈α
the␈αability␈α
to␈α
make␈α
statements␈αabout␈α
the
␈↓ α∧␈↓existence␈α
of␈α
an␈α
answer␈α
that␈αsatisfies␈α
several␈α
subgoals␈α
simultaneously.␈α
 Each␈αsubgoal
␈↓ α∧␈↓may␈αbe␈αsatisfied␈αby␈αa␈αset␈αof␈αanswers;␈αwe␈αwant␈αan␈αelement␈αof␈αthe␈αintersection␈αof␈αthese
␈↓ α∧␈↓sets.



␈↓ α∧␈↓␈↓ αdThere␈α↔are␈α↔several␈α⊗ways␈α↔of␈α↔improving␈α⊗the␈α↔efficiency␈α↔of␈α↔the␈α⊗generated
␈↓ α∧␈↓programs.␈α We␈αintend␈αto␈αincorporate␈αsome␈αanalysis␈αto␈αdetermine␈αthe␈αbest␈αordering␈α
of
␈↓ α∧␈↓alternatives␈αand␈αof␈αsubgoals␈α
within␈αalternatives␈α(20).␈α We␈α
would␈αalso␈αlike␈αto␈α
generate
␈↓ α∧␈↓programs to optimize the source language programs for particular target languages.

␈↓ α∧␈↓␈↓ αdThe␈αmost␈αdramatic␈αimprovement␈αto␈αthe␈αsystem␈αwould␈αbe␈αthe␈αdevelopment␈αof
␈↓ α∧␈↓a␈α∩program␈α∩that␈α∩could␈α∪automatically␈α∩generate␈α∩the␈α∩mapping␈α∩from␈α∪intermediate␈α∩to
␈↓ α∧␈↓target␈αlanguage␈α
from␈αa␈α
formal␈αspecification␈α
of␈αthe␈α
syntax␈αand␈α
semantics␈αof␈αthe␈α
target
␈↓ α∧␈↓language.

␈↓ α∧␈↓␈↓ αdThe␈α⊂sobering␈α⊂fact␈α⊂remains␈α∂that␈α⊂regardless␈α⊂of␈α⊂how␈α∂(or␈α⊂when)␈α⊂we␈α⊂arrive␈α∂at
␈↓ α∧␈↓specifications␈α
for␈α
a␈α
program,␈α
we␈α
can␈αhave␈α
no␈α
guarantee␈α
of␈α
their␈α
correctness␈α
(in␈αthe
␈↓ α∧␈↓sense␈αthat␈αwe␈αhave␈αboth␈αa␈αtrue␈αand␈αcomplete␈αspecification␈αof␈αthe␈αproblem␈αwe␈αhad␈αin
␈↓ α∧␈↓mind),␈α
and␈α
any␈α
attempt␈αat␈α
verification␈α
of␈α
a␈α
program␈αis␈α
simply␈α
a␈α
proof␈αof␈α
equivalence
␈↓ α∧␈↓of␈α∩program␈α∩and␈α∩specifications.␈α∩ We␈α∩simply␈α∪do␈α∩the␈α∩best␈α∩we␈α∩can␈α∩to␈α∪increase␈α∩our
␈↓ α∧␈↓confidence that our programs accomplish their intended purpose.











␈↓ α∧␈↓␈↓	Bibliography␈↓













␈↓ α∧␈↓[1]␈↓ β4 Allen,␈α~J.␈α~R.,␈α~␈↓αAnatomy␈α~of␈α~LISP␈↓.␈α~McGraw-Hill␈α≠Publishing␈α~Co.,
␈↓ α∧␈↓␈↓ ∧∧New York, New York, 1978.


␈↓"∧␈↓ α∧␈↓[2]␈↓ β4 Andreka,␈α
H.␈α
and␈α
I.␈α
Nemeti,␈α
"The␈α
Generalised␈α
Completeness␈α∞of␈α
Horn
␈↓ α∧␈↓␈↓ ∧∧Predicate-Logic␈α∂as␈α∂a␈α∞Programming␈α∂Language",␈α∂D.A.I.␈α∞Research
␈↓ α∧␈↓␈↓ ∧∧Report␈α∞No.␈α∞21,␈α∞Department␈α∞of␈α∞Artificial␈α∞Intelligence,␈α
University
␈↓ α∧␈↓␈↓ ∧∧of Edinburgh, March, 1976.


␈↓"∧␈↓ α∧␈↓[3]␈↓ β4 Balzer,␈α⊗R.␈α⊗M.,␈α⊗N.␈α⊗M.␈α⊗Goldman,␈α⊗and␈α⊗D.S.␈α⊗Wile,␈α⊗"Informality␈α∃in
␈↓ α∧␈↓␈↓ ∧∧Program␈α~Specifications",␈α~University␈α~of␈α~Southern␈α~California
␈↓ α∧␈↓␈↓ ∧∧Information Sciences Institute, ISI/RR-77-59, April, 1977.


␈↓"∧␈↓ α∧␈↓[4]␈↓ β4 Bauer,␈α∞F.␈α∞L.,␈α∞H.␈α∞Partsch,␈α∞P.␈α∞Pepper,␈α∞and␈α∞H.␈α∞W␈↓λ:␈↓ossner,␈α∞"Notes␈α∞on␈α∞the
␈↓ α∧␈↓␈↓ ∧∧Project␈α
                 CIP:␈α
Outline␈α
of␈α
a␈α
Transformation␈αSystem",
␈↓ α∧␈↓␈↓ ∧∧TUM-INFO-7729,␈α⊗        Institut␈α⊗Fur␈α↔Informatik,␈α⊗Technische
␈↓ α∧␈↓␈↓ ∧∧Universit␈↓λ:␈↓at M␈↓λ:␈↓unchen,         July, 1977.


␈↓"∧␈↓ α∧␈↓[5]␈↓ β4 Beach,␈α⊃B.,␈α⊃"Transforming␈α⊃Predicate␈α⊃Calculus␈α⊃Statements␈α⊃Into␈α⊂Horn
␈↓ α∧␈↓␈↓ ∧∧Clauses",␈α∀                Senior␈α∀Thesis,␈α∀University␈α∀of␈α∀California,
␈↓ α∧␈↓␈↓ ∧∧Santa Cruz, June, 1979.



␈↓ α∧␈↓[6]␈↓ β4 Biermann,␈α∪A.␈α∪W.,␈α∀and␈α∪R.␈α∪Krishnaswamy,␈α∀"Constructing␈α∪Programs
␈↓ α∧␈↓␈↓ ∧∧From␈α∩                Example␈α⊃Computations",␈α∩␈↓αIEEE␈α⊃Transactions
␈↓ α∧␈↓α␈↓ ∧∧on Software Engineering␈↓,                 vol. 2, no. 3, Sept., 1976.


␈↓"∧␈↓ α∧␈↓[7]␈↓ β4 Buchanan,␈α⊂J.␈α⊃R.,␈α⊂"A␈α⊂Study␈α⊃in␈α⊂Automatic␈α⊃Programming",␈α⊂AIM-245,
␈↓ α∧␈↓␈↓ ∧∧STAN-CS-74-458,␈α→        Ph.D.␈α→Thesis,␈α→Stanford␈α→University,
␈↓ α∧␈↓␈↓ ∧∧May, 1974.


␈↓"∧␈↓ α∧␈↓[8]␈↓ β4 Buchanan,␈α≠J.␈α≠R.,␈α≠and␈α≠D.␈α≠C.␈α≠Luckham,␈α≠"On␈α≠Automating␈α~the
␈↓ α∧␈↓␈↓ ∧∧Construction␈α⊂of␈α⊂Programs",␈α⊂        SAIL␈α⊂AIM-236,␈α⊂STAN-CS-
␈↓ α∧␈↓␈↓ ∧∧74-433, Stanford University, May, 1974.


␈↓"∧␈↓ α∧␈↓[9]␈↓ β4 Burstall,␈α_R.␈α_M.,␈α_and␈α_J.␈α_Darlington,␈α_"Some␈α_Transformations␈α↔for
␈↓ α∧␈↓␈↓ ∧∧Developing␈α                Recursive␈αPrograms",␈α␈↓αProceedings␈α
of␈αthe
␈↓ α∧␈↓α␈↓ ∧∧International␈α∩Conference␈α∪                on␈α∩Reliable␈α∪Software␈↓,␈α∩Los
␈↓ α∧␈↓␈↓ ∧∧Angeles, Ca., 1975.


␈↓"∧␈↓ α∧␈↓[10]␈↓ β4 Burstall,␈α∩R.␈α∩M.,␈α⊃and␈α∩J.␈α∩Darlington,␈α⊃"A␈α∩Transformation␈α∩System␈α⊃for
␈↓ α∧␈↓␈↓ ∧∧Developing␈α∂        Recursive␈α∂Programs",␈α∂D.A.I.␈α∂Research␈α∞Report
␈↓ α∧␈↓␈↓ ∧∧No.19,         University of Edinburgh, March, 1976.


␈↓"∧␈↓ α∧␈↓[11]␈↓ β4 Clark,␈α∞K.,␈α∞"Synthesis␈α∞and␈α∞Verification␈α∞of␈α∞Logic␈α∂Programs",␈α∞Research
␈↓ α∧␈↓␈↓ ∧∧report,                         CCD, Imperial College, 1977.


␈↓"∧␈↓ α∧␈↓[12]␈↓ β4 Clark,␈α∃K.,␈α⊗and␈α∃J.␈α⊗Darlington,␈α∃"Algorithm␈α⊗Classification␈α∃Through
␈↓ α∧␈↓␈↓ ∧∧Synthesis",␈α$                Imperial␈α$College␈α$of␈α%Science␈α$and
␈↓ α∧␈↓␈↓ ∧∧Technology,␈α_London,␈α_June,␈α↔1978,␈α_                 to␈α_appear␈α↔in
␈↓ α∧␈↓␈↓ ∧∧␈↓αComputer Journal␈↓.


␈↓"∧␈↓ α∧␈↓[13]␈↓ β4 Clark,␈α∂K.,␈α⊂and␈α∂S.␈α⊂Sickel,␈α∂"Predicate␈α∂Logic:␈α⊂A␈α∂Calculus␈α⊂for␈α∂Deriving
␈↓ α∧␈↓␈↓ ∧∧Programs",␈α ␈↓αProceedings␈α∨of␈α the␈α∨Fifth␈α International␈α∨Joint
␈↓ α∧␈↓α␈↓ ∧∧Conference␈α~                on␈α~Artificial␈α≠Intelligence␈↓,␈α~Cambridge,
␈↓ α∧␈↓␈↓ ∧∧Mass., Aug., 1977.


␈↓"∧␈↓ α∧␈↓[14]␈↓ β4 Darlington,␈α
J.,␈α
"Applications␈α
of␈α
Program␈α
Transformation␈α
to␈αProgram
␈↓ α∧␈↓␈↓ ∧∧Synthesis",␈α⊗␈↓αIRIA,␈α⊗Proceedings␈α∃of␈α⊗the␈α⊗Symposium␈α⊗on␈α∃Proving
␈↓ α∧␈↓α␈↓ ∧∧and Improving Programs␈↓, Rocquencourt, France, 1975.



␈↓ α∧␈↓[15]␈↓ β4 Darlington,␈α→J.,␈α_"Program␈α→Transformation␈α_and␈α→Synthesis:␈α_Present
␈↓ α∧␈↓␈↓ ∧∧Capabilities",␈α⊗                DAI␈α∃Report␈α⊗No.␈α∃48,␈α⊗University␈α∃of
␈↓ α∧␈↓␈↓ ∧∧Edinburgh,␈α∃Research␈α∃Report␈α∃No.␈α⊗77/43,␈α∃                Imperial
␈↓ α∧␈↓␈↓ ∧∧College␈α∩of␈α∩Science␈α∩and␈α⊃Technology,␈α∩Dept.␈α∩of␈α∩Computing␈α⊃and
␈↓ α∧␈↓␈↓ ∧∧Control, Sept., 1977.


␈↓"∧␈↓ α∧␈↓[16]␈↓ β4 Darlington,␈α∂J.,␈α∂and␈α∂R.␈α∂M.␈α∂Burstall,␈α∂"A␈α∂System␈α∂Which␈α∂Automatically
␈↓ α∧␈↓␈↓ ∧∧Improves␈α∪        Programs",␈α∩␈↓αActa␈α∪Informatica␈↓,␈α∩vol.␈α∪6,␈α∩pp.41-60,
␈↓ α∧␈↓␈↓ ∧∧1976.


␈↓"∧␈↓ α∧␈↓[17]␈↓ β4 Davis,␈α∞R.␈α∞E.,␈α∞"Deduction,␈α∞Truth,␈α∞and␈α∞Computation",␈α∞Master's␈α
Thesis,
␈↓ α∧␈↓␈↓ ∧∧San Jose State University, San Jose, Ca., 1976.


␈↓"∧␈↓ α∧␈↓[18]␈↓ β4 Dershowitz,␈α!N.,␈α and␈α!Z.␈α Manna,␈α!"On␈α!Automated␈α Structured
␈↓ α∧␈↓␈↓ ∧∧Programming",␈α
                ␈↓αIRIA,␈α
Proceedings␈α
of␈α
the␈αSymposium
␈↓ α∧␈↓α␈↓ ∧∧on␈α
Proving␈α
                and␈α
Improving␈α
Programs␈↓,␈αRocquencourt,
␈↓ α∧␈↓␈↓ ∧∧France, 1975.


␈↓"∧␈↓ α∧␈↓[19]␈↓ β4 van␈αEmden,␈αM.␈αH.,␈αand␈αR.␈αA.␈αKowalski,␈α"The␈αSemantics␈αof␈αPredicate
␈↓ α∧␈↓␈↓ ∧∧Logic␈α∞                as␈α∞a␈α∞Programming␈α∂Language",␈α∞Memorandum
␈↓ α∧␈↓␈↓ ∧∧MIP-R-103,␈α%School␈α%of␈α%                Artificial␈α$Intelligence,
␈↓ α∧␈↓␈↓ ∧∧University of Edinburgh, Feb., 1974.


␈↓"∧␈↓ α∧␈↓[20]␈↓ β4 Franusich,␈α∞M.,␈α∂"Analysis␈α∞of␈α∞Logic␈α∂Programs␈α∞for␈α∞Static␈α∂and␈α∞Dynamic
␈↓ α∧␈↓␈↓ ∧∧Subgoal␈α?␈α≡                Selection",␈α?␈α∨Senior␈α?␈α≡Thesis,
␈↓ α∧␈↓␈↓ ∧∧University of California, Santa Cruz, June, 1979.


␈↓"∧␈↓ α∧␈↓[21]␈↓ β4 Gerhart,␈α∪S.␈α∀L.,␈α∪"Correctness-Preserving␈α∀Program␈α∪Transformations",
␈↓ α∧␈↓␈↓ ∧∧␈↓αProceedings␈α∞        of␈α
the␈α∞2nd␈α∞ACM␈α
Symposium␈α∞on␈α∞Principles␈α
of
␈↓ α∧␈↓α␈↓ ∧∧Programming Languages␈↓,         pp.54-66, January, 1975.


␈↓"∧␈↓ α∧␈↓[22]␈↓ β4 Goldman,␈α⊂N.␈α⊂M.,␈α⊂R.␈α⊂M.␈α⊂Balzer,␈α⊂and␈α⊂D.␈α⊂S.␈α⊂Wile,␈α⊂"The␈α⊂Inference␈α∂of
␈↓ α∧␈↓␈↓ ∧∧Domain␈α%Structure␈α$from␈α%Informal␈α%Process␈α$Descriptions",
␈↓ α∧␈↓␈↓ ∧∧␈↓αProceedings␈α∀                of␈α∀the␈α∀Workshop␈α∃on␈α∀Pattern-Directed
␈↓ α∧␈↓α␈↓ ∧∧Inference Systems␈↓,                 Honolulu, May, 1978.


␈↓"∧␈↓ α∧␈↓[23]␈↓ β4 Gordon,␈α↔M.,␈α_R.␈α↔Milner,␈α↔and␈α_C.␈α↔Wadsworth,␈α_"Edinburgh␈α↔LCF",
␈↓ α∧␈↓␈↓ ∧∧Internal␈α≡Report␈α≡                CSR-11-77␈α≥Part␈α≡1,␈α≡Dept.␈α≥of



␈↓ α∧␈↓␈↓ ∧∧Computer␈α∪Science,␈α∪University␈α∪of␈α∪                Edinburgh,␈α∪Sept
␈↓ α∧␈↓␈↓ ∧∧1977.


␈↓"∧␈↓ α∧␈↓[24]␈↓ β4 Green,␈α⊂C.␈α⊂C.,␈α⊂"A␈α⊃Summary␈α⊂of␈α⊂the␈α⊂PSI␈α⊂Program␈α⊃Synthesis␈α⊂System",
␈↓ α∧␈↓␈↓ ∧∧␈↓αProceedings␈α_of␈α↔the␈α_Fifth␈α↔International␈α_Joint␈α_Conference␈α↔on
␈↓ α∧␈↓α␈↓ ∧∧Artificial Intelligence␈↓, Cambridge, Mass., August 1977.


␈↓"∧␈↓ α∧␈↓[25]␈↓ β4 Hardy,␈αS.,␈α"Synthesis␈αof␈αLISP␈αFunctions␈αfrom␈αExamples",␈α␈↓αProceedings
␈↓ α∧␈↓α␈↓ ∧∧of␈α↔                the␈α↔Fourth␈α⊗International␈α↔Joint␈α↔Conference␈α⊗on
␈↓ α∧␈↓α␈↓ ∧∧Artificial␈α≠                Intelligence␈↓,␈α≠Tbilisi,␈α≤Georgia,␈α≠U.S.S.R.,
␈↓ α∧␈↓␈↓ ∧∧Sept., 1975.


␈↓"∧␈↓ α∧␈↓[26]␈↓ β4 Heidorn,␈αG.␈α
E.,␈α"Automatic␈α
Programming␈αThrough␈αNatural␈α
Language
␈↓ α∧␈↓␈↓ ∧∧Dialogue:␈α#A␈α#Survey",␈α#␈↓αIBM␈α#Journal␈α#of␈α$Research␈α#and
␈↓ α∧␈↓α␈↓ ∧∧Development␈↓,                 vol. 20, no. 4, July, 1976.


␈↓"∧␈↓ α∧␈↓[27]␈↓ β4 von␈α∀Henke,␈α∀F.,␈α∀"On␈α∪Generating␈α∀Programs␈α∀from␈α∀Data␈α∀Types:␈α∪An
␈↓ α∧␈↓␈↓ ∧∧Approach␈α?␈α¬                to␈α?␈αεAutomatic␈α?␈α¬Programming",
␈↓ α∧␈↓␈↓ ∧∧␈↓αIRIA,␈αProceedings␈αof␈αthe␈αSymposium␈αon␈αProving␈α                and
␈↓ α∧␈↓α␈↓ ∧∧Improving Programs␈↓, Rocquencourt, France, 1975.


␈↓"∧␈↓ α∧␈↓[28]␈↓ β4 Igarashi,␈αS.,␈α
R.␈αL.␈α
London,␈αand␈αD.␈α
C.␈αLuckham,␈α
"Automatic␈αProgram
␈↓ α∧␈↓␈↓ ∧∧Verification␈α≤I:␈α≠A␈α≤Logical␈α≠Basis␈α≤and␈α≤its␈α≠Implementation",
␈↓ α∧␈↓␈↓ ∧∧␈↓αActa Informatica␈↓, vol. 4, pp. 145-182, 1975.


␈↓"∧␈↓ α∧␈↓[29]␈↓ β4 Kowalski,␈α#R.,␈α#"Predicate␈α"Logic␈α#as␈α#Programming␈α"Language",
␈↓ α∧␈↓␈↓ ∧∧␈↓αProceedings␈α_                IFIP␈α_74␈↓,␈α_North-Holland␈α_Publishing
␈↓ α∧␈↓␈↓ ∧∧Company, 1974.


␈↓"∧␈↓ α∧␈↓[30]␈↓ β4 Lee,␈α∃R.␈α∀C.␈α∃T.,␈α∃and␈α∀S.␈α∃K.␈α∀Chang,␈α∃"Structured␈α∃Programming␈α∀and
␈↓ α∧␈↓␈↓ ∧∧Automatic␈α∂Program␈α∂Synthesis",␈α∞␈↓αProceedings␈α∂of␈α∂a␈α∂Symposium␈α∞on
␈↓ α∧␈↓α␈↓ ∧∧Very High Level Languages␈↓, Santa Monica, Ca., 1974.


␈↓"∧␈↓ α∧␈↓[31]␈↓ β4 Lenat,␈α
D.␈α
B.,␈α
"Synthesis␈αof␈α
Large␈α
Programs␈α
from␈α
Specific␈αDialogues",
␈↓ α∧␈↓␈↓ ∧∧␈↓αIRIA,␈αProceedings␈αof␈αthe␈αSymposium␈αon␈αProving␈α                and
␈↓ α∧␈↓α␈↓ ∧∧Improving Programs␈↓, Rocquencourt, France, 1975.



␈↓ α∧␈↓[32]␈↓ β4 Loveman,␈α≡D.␈α≥B.,␈α≡"Program␈α≥Improvement␈α≡by␈α≥Source-to-Source
␈↓ α∧␈↓␈↓ ∧∧Transformation",␈α∩        ␈↓αJournal␈α∩of␈α⊃the␈α∩ACM␈α∩␈↓↓24:1␈↓,␈α⊃pp.121-145,
␈↓ α∧␈↓␈↓ ∧∧1977.


␈↓"∧␈↓ α∧␈↓[33]␈↓ β4 Manna,␈αZ.␈αand␈αR.␈αWaldinger,␈α"The␈αAutomatic␈αSynthesis␈αof␈αRecursive
␈↓ α∧␈↓␈↓ ∧∧Programs",␈α↔        ␈↓αProceedings␈α↔of␈α↔the␈α↔Symposium␈α↔on␈α_AI␈α↔and
␈↓ α∧␈↓α␈↓ ∧∧Programming␈α?␈α→Languages␈↓,␈α?␈α→        SIGPLAN/SIGART
␈↓ α∧␈↓␈↓ ∧∧NOTICES/NEWSLETTER␈α→Vol.␈α→12,␈α→No.␈α→8,␈α→August,␈α→1977/
␈↓ α∧␈↓␈↓ ∧∧No. 64, August, 1977.


␈↓"∧␈↓ α∧␈↓[34]␈↓ β4 Manna,␈α
Z.␈α
and␈α
R.␈α
Waldinger,␈α
"Synthesis:␈α
Dreams␈α
=>␈α
Programs",␈α
AIM-
␈↓ α∧␈↓␈↓ ∧∧302,␈α∩        STAN-CS-77-630,␈α∩Stanford␈α∩University,␈α∩November,
␈↓ α∧␈↓␈↓ ∧∧1977.


␈↓"∧␈↓ α∧␈↓[35]␈↓ β4 McCarthy,␈α⊗J.,␈α⊗and␈α⊗C.␈α⊗Talcott,␈α⊗␈↓αLISP␈α⊗Programming␈α↔and␈α⊗Proving␈↓.
␈↓ α∧␈↓␈↓ ∧∧To be published.


␈↓"∧␈↓ α∧␈↓[36]␈↓ β4 Sickel,␈αS.,␈α"Invertibility␈αof␈αLogic␈αPrograms",␈αTechnical␈αReport␈αNo.␈α78-
␈↓ α∧␈↓␈↓ ∧∧8-005,␈α                University␈αof␈αCalifornia,␈αSanta␈αCruz,␈αAugust,
␈↓ α∧␈↓␈↓ ∧∧1978.


␈↓"∧␈↓ α∧␈↓ [37]␈↓ β4 Slagle,␈α∀J.␈α∪R.,␈α∀"Experiments␈α∪with␈α∀a␈α∀Deductive␈α∪Question-Answering
␈↓ α∧␈↓␈↓ ∧∧Program",␈α↔                ␈↓αCommunications␈α_of␈α↔the␈α_Association␈α↔for
␈↓ α∧␈↓α␈↓ ∧∧Computing Machinery␈↓, Vol. 8,                 No. 12, Dec., 1965.


␈↓"∧␈↓ α∧␈↓ [38]␈↓ β4 Summers,␈α∩P.␈α∩D.,␈α∪"A␈α∩Methodology␈α∩for␈α∩LISP␈α∪Program␈α∩Construction
␈↓ α∧␈↓␈↓ ∧∧from␈α$Examples",␈α%                ␈↓αJournal␈α$of␈α%Association␈α$for
␈↓ α∧␈↓α␈↓ ∧∧Computing Machinery␈↓, vol. 24, no. 1,                 Jan., 1977.


␈↓"∧␈↓ α∧␈↓ [39]␈↓ β4 Wile,␈α→D.␈α→S.,␈α_R.␈α→M.␈α→Balzer,␈α_and␈α→N.␈α→M.␈α→Goldman,␈α_"Automated
␈↓ α∧␈↓␈↓ ∧∧Derivation␈α~                of␈α≠Program␈α~Control␈α≠Structure␈α~from
␈↓ α∧␈↓␈↓ ∧∧Natural␈α:Language␈α:Program␈α9                Descriptions",
␈↓ α∧␈↓␈↓ ∧∧␈↓αProceedings␈α?␈αεof␈α?␈απthe␈α?␈αεSymposium␈α?␈απon␈α?␈αεArtificial
␈↓ α∧␈↓α␈↓ ∧∧Intelligence␈α"and␈α#Programming␈α"Languages␈↓,␈α#University␈α"of
␈↓ α∧␈↓␈↓ ∧∧Rochester,                 N.Y., Aug., 1977.


␈↓"∧␈↓ α∧␈↓ [40]␈↓ β4 Ulrich,␈α→J.␈α→W.,␈α→and␈α_R.␈α→Moll,␈α→"Program␈α→Synthesis␈α→by␈α_Analogy",
␈↓ α∧␈↓␈↓ ∧∧␈↓αProceedings␈α?␈αεof␈α?␈απthe␈α?␈αεSymposium␈α?␈απon␈α?␈αεArtificial



␈↓ α∧␈↓α␈↓ ∧∧Intelligence␈α"and␈α#Programming␈α"Languages␈↓,␈α#University␈α"of
␈↓ α∧␈↓␈↓ ∧∧Rochester,                 N.Y., Aug., 1977.



␈↓ α∧␈↓	pub is a crock



␈↓ α∧␈↓pub is more of a crock



␈↓ α∧␈↓page it











␈↓ α∧␈↓	␈↓ βPT A B L E   O F   C O N T E N T S 












␈↓ α∧␈↓␈↓↓BIBLIOGRAPHY␈↓ 
E8␈↓




␈↓ α∧␈↓␈↓↓APPENDICES␈↓